#include "decomp.h"
#include "cktsat/cktcover.h"
#include <iostream>
#include <utility>

using std::cout;
using std::endl;

extern void get_connect_pair( vector<std::pair<unsigned,unsigned> > & p , Bind & x , unsigned var );

// similar to path reduction
static unsigned reduction( unsigned ** base , unsigned i , unsigned j )
{
   if( base[i][j] == i ) return i;
   return reduction( base , base[i][j] , j );
}
static void basevar( unsigned ** base , Bind & x , InputInfo ** in , unsigned fvar , unsigned andFlag )
{
   vector<std::pair<unsigned,unsigned> > eqpair[fvar];
   for( unsigned i = 0 ; i < fvar ; ++ i )
      get_connect_pair( eqpair[i] , x , i );

   for( unsigned i = 0 ; i < x.size() ; ++ i ){
      base[i] = new unsigned[andFlag];
      for( unsigned j = 0 ; j < andFlag ; ++ j )
         base[i][j] = i ;
   }
   for( unsigned i = 0 ; i < fvar ; ++ i )
      for( unsigned j = 0 ; j < andFlag ; ++ j )
         if( in[i][j].connect )
            for( unsigned k = 0 ; k < eqpair[i].size() ; ++ k )
            {
               unsigned & x =  base[ eqpair[i][k].first ][j] , &y= base[ eqpair[i][k].second ][j];
               if(x<y) y=x; else x=y;
            }
   for( unsigned i = 0 ; i < x.size() ; ++ i ) 
      for( unsigned j = 0 ; j < andFlag ; ++ j )
         base[i][j] = reduction( base , i , j );
}
static unsigned baselit( Lit *** lits , unsigned fvar , unsigned andFlag , UnsatBind & x , InputInfo ** in , vector<unsigned> & var2sup , vector<unsigned> & varflag )
{
   unsigned nvar=0 , SETTED = 0xFFFFFFFF;
   unsigned *** base = new unsigned ** [x.size()];
   
   for( unsigned i = 0 ; i < x.size() ; ++ i ) { 
      lits[i]=allocate(x[i].size(),andFlag,Lit(-1,0));
      base[i] = new unsigned * [x[i].size()];
      basevar( base[i] , x[i] , in , fvar ,andFlag );
   }
   //allocate the base variable
   for( unsigned i = 0 ; i < andFlag ; ++ i )
      if( in[x.pivot][i].connect )
      {
         for( unsigned j = 0 ; j < x.common.size() ; ++ j )
         {
            for( unsigned k = 0 ; k < x.common[j].size() ; ++ k )
            {
               std::pair<unsigned,unsigned> y= x.common[j][k];
               unsigned z = base[y.first][y.second][i];
               if( base[y.first][z][i] == SETTED ) continue;
               base[y.first][z][i] = SETTED;
               lits[y.first][z][i] = Lit( nvar , 0 );
            }
            var2sup.push_back( i );
            nvar +=1;
         }
      }
   varflag.push_back( nvar );
   for( unsigned i = 0 ; i < x.size() ; ++ i ){
      for( unsigned j = 0; j < x[i].size() ; ++ j )
         for( unsigned k = 0 ; k < andFlag ; ++ k ) 
            if( base[i][j][k] == j )
               base[i][j][k] = SETTED , lits[i][j][k] = Lit( nvar ++ , 0 );
      varflag.push_back( nvar );
   }
   
   for( unsigned i = 0 ; i < x.size() ; ++ i )
      for( unsigned j = 0 ; j < x[i].size() ; ++ j )
         for( unsigned k = 0 ; k < andFlag ; ++ k )
            if( base[i][j][k] != SETTED )
               lits[i][j][k] = lits[i][ base[i][j][k] ][k];
   
   for( unsigned i = 0 ; i < x.size() ; ++ i ) 
      deallocate( base[i] , x[i].size() );

   return nvar;
}
static bool check_lit( Lit ** lits , unsigned fvar ,unsigned andFlag , Bind & x , InputInfo ** in , unsigned idx )
{
   vector< std::pair<unsigned,unsigned> > eqpair;
   get_connect_pair( eqpair , x , idx );
   
   for( unsigned i = 0 ; i < andFlag ; ++ i )
      if( in[idx][i].connect )
        for( unsigned j = 0 ; j < eqpair.size() ; ++ j )
           if( lits[ eqpair[j].first ][i] != lits[ eqpair[j].second ][i] )
              return false;
   return true;
}
static bool check_lit( Lit ** lits,  unsigned fvar ,unsigned andFlag , Bind & x , InputInfo ** in )
{
   for( unsigned i = 0 ; i < fvar ; ++ i )
      if( check_lit( lits , fvar , andFlag , x , in , i ) == false ) return false;
   return true;
}
static bool check_lit( Lit *** lits , unsigned fvar , unsigned andFlag , UnsatBind & x , InputInfo ** in )
{
   for( unsigned i = 0 ; i < x.size() ; ++ i )
      if( check_lit( lits[i] , fvar ,andFlag , x[i] , in ) == false )return false;
   for( unsigned i = 0 ; i < andFlag ; ++ i )
      if( in[x.pivot][i].connect )
      {
         for( unsigned j = 0 ; j < x.common.size() ; ++ j )
         {
            std::pair<unsigned,unsigned> ref = x.common[j][0];
            for( unsigned k = 1 ; k < x.common[j].size() ; ++ k )
            {
               std::pair<unsigned,unsigned> y = x.common[j][k];
               if( lits[ref.first][ref.second][i] != lits[y.first][y.second][i])
                  return false;
            }
         }
      }
   return true;
}
static void add_constraint( MinisatProof::Solver & s , CktCover * F , CktCover & ckt , BindUnit & x , Lit * lits )
{
   
}
static void add_constraint( MinisatProof::Solver & s , CktCover * F , CktCover & ckt , Bind & x , Lit ** lits )
{
   for( unsigned i = 0 ; i< x.size() ; ++ i )
      add_constraint( s ,F , ckt , x[i] , lits[i] );
}
static void decomposition( CktCover * F , CktCover & ckt , UnsatBind & x , InputInfo ** in )
{
   unsigned fvar = x[0][0].size();
   unsigned andFlag = ckt._andFlag;
  
   Lit *** lits = new Lit ** [ x.size() ];
   vector<unsigned> var2sup;
   vector<unsigned> varflag;
   unsigned nvar = baselit( lits , fvar , andFlag , x , in , var2sup , varflag );
   assert( check_lit( lits , fvar , andFlag , x , in ) );

   MinisatProof::Solver s;
   while( s.nVars() != nvar ) s.newVar();
   s.proof = new MinisatProof::Proof();

   for( unsigned i = 0 ; i < x.size() ; ++i ) 
   {
      add_constraint( s , F , ckt , x[i] , lits[i] );
      varflag.push_back( s.nVars() );
   }
   // dump the constraint 
   // generate interpolant 
   // reconstruct the fx 
}

